Unifying Theories in Isabelle/HOL
Identifieur interne : 000124 ( Main/Exploration ); précédent : 000123; suivant : 000125Unifying Theories in Isabelle/HOL
Auteurs : Abderrahmane Feliachi [France] ; Marie-Claude Gaudel [France] ; Burkhart Wolff [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2010.
English descriptors
- KwdEn :
- Circus , CSP, Isabelle/HOL, Theorem Proving, UTP.
Abstract
Abstract: In this paper, we present various extensions of Isabelle/HOL by theories that are essential for several formal methods. First, we explain how we have developed an Isabelle/HOL theory for a part of the Unifying Theories of Programming (UTP). It contains the theories of alphabetized relations and designs. Then we explain how we have encoded first the theory of reactive processes and then the UTP theory for CSP. Our work takes advantage of the rich existing logical core of HOL. Our extension contains the proofs for most of the lemmas and theorems presented in the UTP book. Our goal is to propose a framework that will allow us to deal with formal methods that are semantically based, partly or totally, on UTP, for instance CSP and Circus . The theories presented here will allow us to make proofs about such specifications and to apply verified transformations on them, with the objective of assisting refinement and test generation.
Url:
DOI: 10.1007/978-3-642-16690-7_9
Affiliations:
Links toward previous steps (curation, corpus...)
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Unifying Theories in Isabelle/HOL</title><author><name sortKey="Feliachi, Abderrahmane" sort="Feliachi, Abderrahmane" uniqKey="Feliachi A" first="Abderrahmane" last="Feliachi">Abderrahmane Feliachi</name></author><author><name sortKey="Gaudel, Marie Claude" sort="Gaudel, Marie Claude" uniqKey="Gaudel M" first="Marie-Claude" last="Gaudel">Marie-Claude Gaudel</name></author><author><name sortKey="Wolff, Burkhart" sort="Wolff, Burkhart" uniqKey="Wolff B" first="Burkhart" last="Wolff">Burkhart Wolff</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:04FFF401263AA42FBAB822701FA466DB30761B37</idno><date when="2010" year="2010">2010</date><idno type="doi">10.1007/978-3-642-16690-7_9</idno><idno type="url">https://api.istex.fr/document/04FFF401263AA42FBAB822701FA466DB30761B37/fulltext/pdf</idno><idno type="wicri:Area/Main/Corpus">001264</idno><idno type="wicri:explorRef" wicri:stream="Main" wicri:step="Corpus" wicri:corpus="ISTEX">001264</idno><idno type="wicri:Area/Main/Curation">001264</idno><idno type="wicri:Area/Main/Exploration">000124</idno><idno type="wicri:explorRef" wicri:stream="Main" wicri:step="Exploration">000124</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Unifying Theories in Isabelle/HOL</title><author><name sortKey="Feliachi, Abderrahmane" sort="Feliachi, Abderrahmane" uniqKey="Feliachi A" first="Abderrahmane" last="Feliachi">Abderrahmane Feliachi</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay</wicri:regionArea><placeName><region type="region" nuts="2">Île-de-France</region><settlement type="city">Orsay</settlement></placeName></affiliation><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>CNRS, F-91405, Orsay</wicri:regionArea><placeName><region type="region" nuts="2">Île-de-France</region><settlement type="city">Orsay</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Gaudel, Marie Claude" sort="Gaudel, Marie Claude" uniqKey="Gaudel M" first="Marie-Claude" last="Gaudel">Marie-Claude Gaudel</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay</wicri:regionArea><placeName><region type="region" nuts="2">Île-de-France</region><settlement type="city">Orsay</settlement></placeName></affiliation><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>CNRS, F-91405, Orsay</wicri:regionArea><placeName><region type="region" nuts="2">Île-de-France</region><settlement type="city">Orsay</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Wolff, Burkhart" sort="Wolff, Burkhart" uniqKey="Wolff B" first="Burkhart" last="Wolff">Burkhart Wolff</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Laboratoire LRI, UMR8623, Univ Paris-Sud, F-91405, Orsay</wicri:regionArea><placeName><region type="region" nuts="2">Île-de-France</region><settlement type="city">Orsay</settlement></placeName></affiliation><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>CNRS, F-91405, Orsay</wicri:regionArea><placeName><region type="region" nuts="2">Île-de-France</region><settlement type="city">Orsay</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2010</date></imprint><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series><idno type="istex">04FFF401263AA42FBAB822701FA466DB30761B37</idno><idno type="DOI">10.1007/978-3-642-16690-7_9</idno><idno type="ChapterID">Chap9</idno><idno type="ChapterID">9</idno></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term> Circus </term><term>CSP</term><term>Isabelle/HOL</term><term>Theorem Proving</term><term>UTP</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: In this paper, we present various extensions of Isabelle/HOL by theories that are essential for several formal methods. First, we explain how we have developed an Isabelle/HOL theory for a part of the Unifying Theories of Programming (UTP). It contains the theories of alphabetized relations and designs. Then we explain how we have encoded first the theory of reactive processes and then the UTP theory for CSP. Our work takes advantage of the rich existing logical core of HOL. Our extension contains the proofs for most of the lemmas and theorems presented in the UTP book. Our goal is to propose a framework that will allow us to deal with formal methods that are semantically based, partly or totally, on UTP, for instance CSP and Circus . The theories presented here will allow us to make proofs about such specifications and to apply verified transformations on them, with the objective of assisting refinement and test generation.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Île-de-France</li></region><settlement><li>Orsay</li></settlement></list><tree><country name="France"><region name="Île-de-France"><name sortKey="Feliachi, Abderrahmane" sort="Feliachi, Abderrahmane" uniqKey="Feliachi A" first="Abderrahmane" last="Feliachi">Abderrahmane Feliachi</name></region><name sortKey="Feliachi, Abderrahmane" sort="Feliachi, Abderrahmane" uniqKey="Feliachi A" first="Abderrahmane" last="Feliachi">Abderrahmane Feliachi</name><name sortKey="Feliachi, Abderrahmane" sort="Feliachi, Abderrahmane" uniqKey="Feliachi A" first="Abderrahmane" last="Feliachi">Abderrahmane Feliachi</name><name sortKey="Gaudel, Marie Claude" sort="Gaudel, Marie Claude" uniqKey="Gaudel M" first="Marie-Claude" last="Gaudel">Marie-Claude Gaudel</name><name sortKey="Gaudel, Marie Claude" sort="Gaudel, Marie Claude" uniqKey="Gaudel M" first="Marie-Claude" last="Gaudel">Marie-Claude Gaudel</name><name sortKey="Gaudel, Marie Claude" sort="Gaudel, Marie Claude" uniqKey="Gaudel M" first="Marie-Claude" last="Gaudel">Marie-Claude Gaudel</name><name sortKey="Wolff, Burkhart" sort="Wolff, Burkhart" uniqKey="Wolff B" first="Burkhart" last="Wolff">Burkhart Wolff</name><name sortKey="Wolff, Burkhart" sort="Wolff, Burkhart" uniqKey="Wolff B" first="Burkhart" last="Wolff">Burkhart Wolff</name><name sortKey="Wolff, Burkhart" sort="Wolff, Burkhart" uniqKey="Wolff B" first="Burkhart" last="Wolff">Burkhart Wolff</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Wicri/explor/CircusV2/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000124 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000124 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Wicri
|area= CircusV2
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:04FFF401263AA42FBAB822701FA466DB30761B37
|texte= Unifying Theories in Isabelle/HOL
}}
| This area was generated with Dilib version V0.6.31. |  |